All right, and then let's continue. Before we actually start with the taboo machine,

if I remember correctly, there were some questions about the homework that was due on Thursday,

or nothing. That was the semantic construction thing.

Yes. All right. I'm just going to open

Open this one for 10.

So one thing you could do,

that's the long-run work.

This one. You could extend the logic, for example, and make another thing here,

which we call, for example, equal. We don't have actually individuals in here. I just have to place

it here. Equal. Something like this. And then we have a rule for that, probably.

So we at some point have a rule. I'm just going to sketch it here.

As for where we would take, for example, a noun phrase to a sentence.

Yeah, so we have drawn this Peter or something like that. And then in the construction,

what we want to do is we have so lambda x, that's the first noun phrase, lambda y,

second noun phrase. And then we just put equal x, y. That's one way of doing it.

I don't remember if this fits quite in the grammar like this, but something like this

would, for example, work. So the same way we have basically, so that's one way. The other way,

if you have,

I think that's a basic idea of this rule. Instead, you could also say we made a verb

phrase out of this. So we say this is a verb phrase. And then you treat this basically the

same way you would treat love or see or something like that as a verb. And map it again to this

equal. Does that help already? Okay. Any other questions about this?

No. Okay. Then I'll, so our goal is not to, right. So the homework for today was to,

let's quickly talk about that as well first, to finish the evaluation thing here. Other

questions about that? No. Okay. It's also not necessary for today really. So the goal today

is that we implement this tableau machine here. It's not really that much code actually. It's

like one of these evaluation thingies. And before I do that, I'll just quickly recap what we've been,

what we went through last week on Thursday. So the first thing that we did is we wrote down the

syntax of the logic the same way as an MMT basically, just a tiny bit different.

So here's our type for propositions. And then we have negation and or application true false.

And here P var for variables. So we just number them one, two, three, four, and so on.

And then we made a predicate here atomic that we'll need that later today,

which tells us whether proposition is atomic or not.

And then we did some evaluation. Basically does this formula evaluate true or false if it's

grounded? That's not that important for today. We made a simplifier that just replaces all the

connectives with and and not. And we started working on some list. So just to get used to lists,

we have this member predicate. We'll get examples. We can use this.

Get more down like this to the level of the list or not.

Yes, then we try to do a better evaluation. That was the homework where we have assignments.

That's not that important. So what you want to do now is we want to make the

tableau machine or the model generation. So just to sketch and sample,

we want, for example, to say if we put A and B or C, and then the double machine would market

is true. And then we would start to like the rules. We would get A true B or C true.

And we split B true C true just as we discussed. And then we get a model.

Let's say one model here we have A true B true. And here we would have a model A true B true.

Those are the two models. So we want to have a mechanism where we put this in and get this out.

We want to get both things. Any ideas how we would get started with this? What pieces do we need?

We need what? Yes, exactly. So we need to somehow write them all down in LP.

And as a start, for example, we would want to have the rule if we have X and Y true,

then somehow we want to have X true, Y true, and then continue with X and Y somehow.